\begin{tabbing}
$\forall$$A$, $B$:Realizer.
\\[0ex]R{-}Feasible($A$)
\\[0ex]$\Rightarrow$ R{-}Feasible($B$)
\\[0ex]$\Rightarrow$ ($\exists$\=$i$,$j$:Id\+
\\[0ex](($\forall$$x$:Id. R{-}has{-}loc($A$;$x$) = $i$ = $x$ $\in$ $\mathbb{B}$)
\\[0ex]\& ($\forall$$x$:Id. R{-}has{-}loc($B$;$x$) = $j$ = $x$ $\in$ $\mathbb{B}$)
\\[0ex]\& ($\neg$($i$ = $j$))
\\[0ex]\& \=$\forall$$k$$\in$dom(R{-}da($A$;$i$)). \+
\\[0ex]
\\[0ex]$T$\==R{-}da($A$;$i$)($k$) $\Rightarrow$ \+
\\[0ex]($\uparrow$isrcv($k$))
\-\\[0ex]$\Rightarrow$ \=(((source(lnk($k$)) = $i$ $\in$ Id) $\Rightarrow$ ($T$ $\subseteq$r R{-}da($B$;destination(lnk($k$)))($k$)?Top))\+
\\[0ex]\& ((destination(lnk($k$)) = $i$ $\in$ Id) $\Rightarrow$ (R{-}da($B$;source(lnk($k$)))($k$)?Void $\subseteq$r $T$)))))
\-\-\-\\[0ex]$\Rightarrow$ $A$ $\parallel$ $B$
\end{tabbing}